package component;

import java.util.ArrayList;

import Prism.core.AbstractImplementation;
import Prism.core.Event;
import Prism.core.PrismConstants;
import basicTypes.OnlineUserRecord;
import basicTypes.Service;
import basicTypes.UserRecord;

public class TransConsistCheck extends AbstractImplementation {

	// prov Name(Event Name)
	public static final String provIsLocked = "isLocked";
	public static final String provAddRequest = "addRequest";
	public static final String provDeleteRequest = "deleteRequest";
	public static final String provCheckRequest = "checkRequest";
	public static final String provGetTime = "getTime";
	public static final String provLockUser = "lockUser";
	public static final String provUnlockUser = "unlockUser";
	public static final String provSubmitUserDataAndOperation = "submitUserDataAndOperation";
	public static final String provObtainAvailablePhoneNumber = "obtainAvailablePhoneNumber";
	public static final String provShowUserData = "showUserData";
	
	//locks: \set PhoneNumber; //users currently being processed
	ArrayList<String> locks;
	
	//currentRequests: \set UserRecordType;//requests being processed
	ArrayList<UserRecord> currentRequests;
	
	//currentRequestsByPhoneNumber: PhoneNumber -> UserRecordType;
	public UserRecord currentRequestsByPhoneNumber(String phoneNumber) {
		int size = currentRequests.size();
		
		for(int i=0; i<size; i++) {
			if(currentRequests.get(i).getPhoneNumber().equals(phoneNumber)) {
				return currentRequests.get(i);
			}
		}
		
		return null;
	}
	
	//Index of currentRequests
	public int currentRequestsIndexByPhoneNumber(String phoneNumber) {
		int size = currentRequests.size();
		
		for(int i=0; i<size; i++) {
			if(currentRequests.get(i).getPhoneNumber().equals(phoneNumber)) {
				return i;
			}
		}
		
		return -1;
	}
	
	// currentTime: Time;
	public int currentTime() {return (int)System.currentTimeMillis()/1000;}

	// Check invariant property
	public boolean checkInvariant() {
		//#locks \eqgreater 0;
		//#currentRequests \eqgreater 0;
		if(locks.size()>=0 && currentRequests.size()>=0) return true;
		return false;
	}
	
	@Override
	public void start() {
		super.start();
		
		// Initialize
		locks = new ArrayList<String>();
		currentRequests = new ArrayList<UserRecord> ();
	}
	
	@Override
	public void handle(Event e) {
		
		// Handle of request of provIsLocked
		if(e.getName().equals(provIsLocked)) {
			String no = (String)e.getParameter("phoneNumber");
			
			Event n = new Event(provIsLocked, PrismConstants.REPLY);
			// post ((id \in locks) \implies (\result=TRUE))
			// \and ((id \not_in locks) \implies (\result=FALSE));
			n.addParameter("boolean", locks.contains(no)?"TRUE":"FALSE");
			this.send(n);
		}
		// Handle of request of provAddRequest
		else if(e.getName().equals(provAddRequest)) {
			UserRecord tempRecord = new UserRecord(
					(String) e.getParameter("time"),
					(String) e.getParameter("name"),
					(String) e.getParameter("amount"),
					(String) e.getParameter("phoneNumber")
					);
			
			// pre (id \in locks) \and (rec \not_in currentRequests);
			if( (locks.contains((String) e.getParameter("phoneNumber")))
				&& (currentRequestsByPhoneNumber((String) e.getParameter("phoneNumber"))==null)){

				// post (rec \in currentRequests) \and (#~currentRequests=#currentRequests+1);
				currentRequests.add(tempRecord);
			}
		}
		// Handle of request of provDeleteRequest
		else if(e.getName().equals(provDeleteRequest)) {

			//pre (id \in locks) \and (rec \in currentRequests);
			if( (locks.contains((String) e.getParameter("phoneNumber")))
					&& (currentRequestsByPhoneNumber((String) e.getParameter("phoneNumber"))!=null)){
				//post (rec \not_in currentRequests) \and (#~currentRequests=#currentRequests-1);
				int index = currentRequestsIndexByPhoneNumber((String) e.getParameter("phoneNumber"));
				currentRequests.remove(index);
			}


		}
		// Handle of request of provCheckRequest
		else if(e.getName().equals(provCheckRequest)) {
			
			//pre (id \in locks) \and (rec \in currentRequests);
			if( (locks.contains((String) e.getParameter("phoneNumber")))
					&& (currentRequestsByPhoneNumber((String) e.getParameter("phoneNumber"))!=null)){
				//DO SOMETHING
			}
		}
		// Handle of request of provGetTime
		else if(e.getName().equals(provGetTime)) {
			
			//post \result = ~currentTime;
			Event n = new Event(provGetTime, PrismConstants.REPLY);
			n.addParameter("time",String.valueOf(currentTime()));
			this.send(n);
		}
		// Handle of request of provLockUser
		else if(e.getName().equals(provLockUser)) {
			
			//pre (id \not_in locks);
			if(locks.contains((String) e.getParameter("phoneNumber"))==false) {
				//post (id \in locks) \and (#~locks=#locks+1);
				locks.add((String) e.getParameter("phoneNumber"));
			}
		}
		// Handle of request of provUnlockUser
		else if(e.getName().equals(provUnlockUser)) {
			
			//pre (id \in locks);
			if(locks.contains((String) e.getParameter("phoneNumber"))) {
			//post (id \not_in locks) \and (#~locks=#locks-1);
				locks.remove((String) e.getParameter("phoneNumber"));
			}
			
		}
		// Handle of request of provSubmitUserDataAndOperation
		else if(e.getName().equals(provSubmitUserDataAndOperation)) {
		}
		// Handle of request of provObtainAvailablePhoneNumber
		else if(e.getName().equals(provObtainAvailablePhoneNumber)) {
			getAvailablePhoneNumber((String) e.getParameter("taskID"));
		}
		// Handle of request of provShowUserData
		else if(e.getName().equals(provShowUserData)) {
			getUserData((String) e.getParameter("phoneNumber"));
		}
		
		// Handle of request reply of NossTransManager.provGetAvailablePhoneNumber
		else if(e.getName().equals(NossTransManager.provGetAvailablePhoneNumber)) {
			Event n = new Event(provObtainAvailablePhoneNumber, PrismConstants.REPLY);
			n.addParameter("phoneNumber", (String)e.getParameter("phoneNumber"));
			this.send(n);

		}
		// Handle of request reply of OnLineDatabase.provGetUserData
		else if(e.getName().equals(OnLineDatabase.provGetUserData)) {
			//Do Something
			System.out.println((String) e.getParameter("name"));
			System.out.println((String) e.getParameter("phoneNumber"));
		}
	}
	
	public void addUser( String phoneNumber, OnlineUserRecord our ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(OnLineDatabase.provAddUser, PrismConstants.REQUEST);
		r.addParameter("time", our.getTime());
		r.addParameter("name", our.getName());
		r.addParameter("amount", our.getAmount());
		r.addParameter("phoneNumber", phoneNumber);
		this.send(r);
	}
	public void deleteUser( String phoneNumber ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(OnLineDatabase.provDeleteUser, PrismConstants.REQUEST);
		r.addParameter("phoneNumber", phoneNumber);
		this.send(r);
	}
	public void updateUser( String phoneNumber, OnlineUserRecord our ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(OnLineDatabase.provUpdateUser, PrismConstants.REQUEST);
		r.addParameter("time", our.getTime());
		r.addParameter("name", our.getName());
		r.addParameter("amount", our.getAmount());
		r.addParameter("phoneNumber", phoneNumber);
		this.send(r);
	}
	public void getAvailablePhoneNumber( String tid ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(NossTransManager.provGetAvailablePhoneNumber, PrismConstants.REQUEST);
		r.addParameter("taskID", tid);
		this.send(r);
	}
	public void getUserData( String phoneNumber ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(OnLineDatabase.provGetUserData, PrismConstants.REQUEST);
		r.addParameter("phoneNumber", phoneNumber);
		this.send(r);
	}
	public void addService( Service s ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(OnLineDatabase.provAddService, PrismConstants.REQUEST);
		r.addParameter("serviceType",s.getServiceType());
		r.addParameter("phoneNumber",s.getPhoneNumber());
		this.send(r);
	}
	public void removeService( Service s ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(OnLineDatabase.provRemoveService, PrismConstants.REQUEST);
		r.addParameter("serviceType",s.getServiceType());
		r.addParameter("phoneNumber",s.getPhoneNumber());
		this.send(r);
	}
	public void addNewNumber( String phoneNumber ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(NossTransManager.provAddNewNumber, PrismConstants.REQUEST);
		r.addParameter("phoneNumber", phoneNumber);
		this.send(r);
	}
	public void deleteExistingNumber( String phoneNumber ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(NossTransManager.provDeleteExistingNumber, PrismConstants.REQUEST);
		r.addParameter("phoneNumber", phoneNumber);
		this.send(r);
	}
	public void lockResource( String phoneNumber, String tid ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(NossTransManager.provLockResource, PrismConstants.REQUEST);
		r.addParameter("phoneNumber", phoneNumber);
		r.addParameter("taskID", tid);
		this.send(r);
	}
	public void unlockResource( String phoneNumber ,String tid ) {
		// send request to upper layer
		Prism.core.Event r = new Prism.core.Event(NossTransManager.provUnlockResource, PrismConstants.REQUEST);
		r.addParameter("phoneNumber", phoneNumber);
		r.addParameter("taskID", tid);
		this.send(r);
	}
}

